Nuprl Definition : w-locl
11,40
postcript
pdf
e
<loc
e'
== loc(
e
) = loc(
e'
) & (time(
e
) < time(
e'
))
latex
clarification:
w-locl(
w
;
e
;
e'
) == w-loc(
w
;
e
) = w-loc(
w
;
e'
)
Id & (w-time(
w
;
e
) < w-time(
w
;
e'
))
latex
Definitions
P
&
Q
,
s
=
t
,
Id
,
loc(
e
)
,
a
<
b
,
time(
e
)
FDL editor aliases
w-locl
origin
Id & (w-time(w; e) < w-time(w; e')) Id & (w-time(w; e) < w-time(w; e'))